<html>
<head><meta charset="utf-8"><title>analysis on MIR · general · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/index.html">general</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/analysis.20on.20MIR.html">analysis on MIR</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="237134839"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/analysis%20on%20MIR/near/237134839" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Andreea <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/analysis.20on.20MIR.html#237134839">(May 03 2021 at 09:29)</a>:</h4>
<p>Hi,</p>
<p>I'd like to build a static analysis tool for MIR (checking for memory bugs when unsafe code messes up things). Is someone kind enough to point me to some tool support for building analysis tools for Rust?</p>
<p>I've been looking at <code>clippy</code>, but  <a href="https://rust-lang.github.io/rfcs/1211-mir.html#which-analyses-are-well-suited-to-the-mir">it seems to be "ill-suited" for MIR analysis</a>. I might need to store state, and refer back to the original Rust code too. </p>
<p>Thanks!</p>



<a name="237138019"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/analysis%20on%20MIR/near/237138019" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Pointerbender <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/analysis.20on.20MIR.html#237138019">(May 03 2021 at 09:58)</a>:</h4>
<p>Hi <span class="user-mention" data-user-id="409570">@Andreea</span> , you could checkout how <a href="https://github.com/rust-lang/miri">Miri</a> does it for inspiration. Miri is also quite good at checking memory bugs that way.</p>



<a name="237139901"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/analysis%20on%20MIR/near/237139901" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Pointerbender <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/analysis.20on.20MIR.html#237139901">(May 03 2021 at 10:17)</a>:</h4>
<p>There is even a <a href="https://publikationen.sulb.uni-saarland.de/handle/20.500.11880/29647">cool thesis</a> available about how the memory safety is checked by Miri in case you're interested (heads up, it's pretty complicated stuff and about ~300 pages). The model described there is called Stacked Borrows, you can find higher level explanations about how it works <a href="https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md">here</a>.</p>



<a name="237165190"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/analysis%20on%20MIR/near/237165190" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Andreea <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/analysis.20on.20MIR.html#237165190">(May 03 2021 at 14:02)</a>:</h4>
<p>Thanks for all the pointers, <span class="user-mention" data-user-id="400735">@Pointerbender</span> . I did check Stack Borrows and its implementation in Miri. Good inspiration! However, these are dynamic approaches, while I am searching for static solutions.</p>



<a name="237169875"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/analysis%20on%20MIR/near/237169875" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Pointerbender <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/analysis.20on.20MIR.html#237169875">(May 03 2021 at 14:34)</a>:</h4>
<p>Hmm I know of only one tool that can do that so far (there might be others, though? I just stumbled into this part of Rust very recently), it's called <a href="https://plv.mpi-sws.org/rustbelt/#project">RustBelt</a> and takes an academic approach of proving that a program can't contain undefined behavior through static analysis. I think it's very promising, but it currently also has some drawbacks. For example, it is only suitable for researchers because it requires a lot of theoretical knowledge to work with (the earlier linked thesis also gives a nice introduction to RustBelt, by the way). Another thing to keep in mind is that it only works on a limited subset of the Rust language (called λRust). I believe that quite recently support for <code>Arc</code>, <code>RefCell</code>, <code>Rc</code> and <code>RwLock</code> was added, and it already had support for <code>Mutex</code> and <code>Cell</code>. They also have a provably safe type of their own which is called <code>GhostCell</code> (<a href="https://plv.mpi-sws.org/rustbelt/ghostcell/paper.pdf">paper</a>), which is very interesting stuff.</p>



<a name="237170259"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/analysis%20on%20MIR/near/237170259" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/analysis.20on.20MIR.html#237170259">(May 03 2021 at 14:37)</a>:</h4>
<p>it's not really a static analysis, proofs in rustbelt (in iris) are fully manual</p>



<a name="237171395"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/analysis%20on%20MIR/near/237171395" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Pointerbender <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/analysis.20on.20MIR.html#237171395">(May 03 2021 at 14:44)</a>:</h4>
<p>Ah that is good to know. So currently it's not yet possible to automatically convert Rust code into a RustBelt representation and run the prover? Rather we would write the manual proof in RustBelt and then manually transcribe that to Rust code once the proof passes?</p>



<a name="237172910"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/analysis%20on%20MIR/near/237172910" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Pointerbender <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/analysis.20on.20MIR.html#237172910">(May 03 2021 at 14:53)</a>:</h4>
<p>(for Rust code that falls inside λRust, that is)</p>



<a name="237335673"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/analysis%20on%20MIR/near/237335673" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> FireFighterDuck <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/analysis.20on.20MIR.html#237335673">(May 04 2021 at 14:39)</a>:</h4>
<p>It's not really a tool per se, but you might want to have a look at <a href="https://hackmd.io/RiztubvfT4eOk4-4nM8Y7Q?view">these slides</a> from the Rust Verification workshop a few weeks ago. They describe how one could use rustc to build analysis/linting/etc. tools using callbacks. I hope that helps.</p>



<a name="237441074"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/analysis%20on%20MIR/near/237441074" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/analysis.20on.20MIR.html#237441074">(May 05 2021 at 04:55)</a>:</h4>
<p>Are any of the rust verification workshop talks online? I was not able to attend but there seemed to be a bunch of interesting things</p>



<a name="237475256"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/analysis%20on%20MIR/near/237475256" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> FireFighterDuck <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/analysis.20on.20MIR.html#237475256">(May 05 2021 at 10:55)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/122651-general/topic/analysis.20on.20MIR/near/237441074">said</a>:</p>
<blockquote>
<p>Are any of the rust verification workshop talks online? I was not able to attend but there seemed to be a bunch of interesting things</p>
</blockquote>
<p>The talks were indeed quite interesting and IIRC all talks were recorded as well. But I don't think that they are already available online. You might need to ask <span class="user-mention" data-user-id="116009">@nikomatsakis</span> about that.</p>



<a name="238355294"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/analysis%20on%20MIR/near/238355294" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/analysis.20on.20MIR.html#238355294">(May 11 2021 at 17:56)</a>:</h4>
<p>the talks have apparently been published today on youtube <a href="https://www.youtube.com/playlist?list=PL85XCvVPmGQiF26DB84AK3i1yjKu52fq_">https://www.youtube.com/playlist?list=PL85XCvVPmGQiF26DB84AK3i1yjKu52fq_</a></p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>